REF, NoConds
\\[0ex]Unfold `\$ab` \$hyp $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$Unfold `\$ab` ( \$hyp)$\cdot$